1. $A$ : Type
\\[0ex]2. $x$ : $A$
\\[0ex]3. $y$ : $A$
\\[0ex]4. $P$ : $A$$\rightarrow\mathbb{P}$
\\[0ex]5. $i$ : $\mathbb{Z}$
\\[0ex]6. $j$ : $\mathbb{Z}$
\\[0ex]7. $P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi )
\\[0ex]$\vdash$  $P$(if ($i$ =$_{0}$ $j$) then $x$ else $y$ fi )